\begin{tabbing}
$\forall$$k$:Knd, $T$, $B$:Type, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it tg}$:Id, $f$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$$B$).
\\[0ex](isrcv($k$) $\Rightarrow$ destination(lnk($k$)) $=$ source($l$) $\in$ Id \& (lnk($k$) $=$ $l$ $\Rightarrow$ $T$ $=$ $B$ \& tag($k$) $=$ ${\it tg}$))
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ Normal($B$)
\\[0ex]$\Rightarrow$ \=sends $k$(v:$T$) on $l$:\+
\\[0ex]tagged([$\langle$${\it tg}$$,\,$$\lambda$$s$,$v$. [$f$($s$,$v$)]$\rangle$],State(${\it ds}$),v):${\it tg}$ : $B$
\\[0ex]$\Vdash$ ${\it es}$.usends1{-}p(${\it es}$;${\it ds}$;$k$;$T$;$l$;${\it tg}$;$B$;$f$)
\-
\end{tabbing}